Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 6 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
G(ok(X)) → G(X)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(G(x1)) = 2·x1
POL(ok(x1)) = 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The set Q is empty.
We have obtained the following QTRS:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 6. This implies Q-termination of R.
The following rules were used to construct the certificate:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
97, 98, 99, 100, 101, 102, 104, 103, 105, 106, 107, 108, 109, 110, 111, 113, 112, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 150, 151, 152, 153, 154, 155, 157
Node 97 is start node and node 98 is final node.
Those nodes are connect through the following edges:
- 97 to 99 labelled proper_1(0)
- 97 to 100 labelled active_1(0), proper_1(0)
- 97 to 101 labelled g_1(0), f_1(0), c'_1(0)
- 97 to 102 labelled c'_1(0)
- 97 to 110 labelled c'_1(1)
- 97 to 109 labelled proper_1(1)
- 97 to 111 labelled c'_1(1)
- 97 to 113 labelled g_1(1)
- 97 to 119 labelled proper_1(2)
- 97 to 120 labelled c'_1(2)
- 97 to 134 labelled c'_1(3)
- 97 to 154 labelled c'_1(4)
- 98 to 98 labelled #_1(0)
- 99 to 98 labelled g_1(0), f_1(0)
- 99 to 106 labelled proper_1(1)
- 99 to 107 labelled g_1(1)
- 99 to 115 labelled proper_1(2)
- 100 to 98 labelled top_1(0)
- 101 to 98 labelled ok_1(0), mark_1(0)
- 101 to 105 labelled proper_1(1), active_1(1)
- 101 to 108 labelled g_1(1), f_1(1)
- 101 to 117 labelled g_1(2)
- 101 to 124 labelled proper_1(3)
- 101 to 128 labelled proper_1(2)
- 102 to 103 labelled g_1(0)
- 102 to 116 labelled proper_1(1)
- 104 to 98 labelled mark_1(0)
- 104 to 105 labelled proper_1(1)
- 103 to 104 labelled f_1(0)
- 103 to 109 labelled proper_1(1)
- 105 to 98 labelled top_1(1)
- 106 to 98 labelled g_1(1), f_1(1)
- 106 to 106 labelled proper_1(1)
- 106 to 107 labelled g_1(1)
- 106 to 115 labelled proper_1(2)
- 107 to 98 labelled mark_1(1)
- 107 to 105 labelled proper_1(1)
- 108 to 98 labelled ok_1(1)
- 108 to 105 labelled active_1(1)
- 108 to 108 labelled g_1(1), f_1(1)
- 108 to 117 labelled g_1(2)
- 108 to 124 labelled proper_1(3)
- 108 to 128 labelled proper_1(2)
- 109 to 105 labelled f_1(1), g_1(1)
- 109 to 124 labelled f_1(1), g_1(1)
- 109 to 128 labelled g_1(1), f_1(1)
- 110 to 105 labelled ok_1(1)
- 110 to 114 labelled active_1(2)
- 110 to 116 labelled ok_1(1)
- 110 to 126 labelled g_1(2)
- 110 to 124 labelled ok_1(1)
- 110 to 128 labelled ok_1(1)
- 110 to 136 labelled f_1(2), g_1(2)
- 110 to 129 labelled f_1(2), g_1(2)
- 110 to 137 labelled g_1(3)
- 110 to 140 labelled proper_1(4)
- 111 to 112 labelled g_1(1)
- 111 to 123 labelled proper_1(2)
- 113 to 105 labelled mark_1(1)
- 113 to 114 labelled proper_1(2)
- 112 to 113 labelled f_1(1)
- 112 to 118 labelled proper_1(2)
- 114 to 98 labelled top_1(2)
- 115 to 105 labelled g_1(2)
- 116 to 109 labelled g_1(1)
- 117 to 105 labelled mark_1(2)
- 117 to 114 labelled proper_1(2)
- 118 to 114 labelled f_1(2)
- 119 to 114 labelled g_1(2)
- 120 to 121 labelled g_1(2)
- 120 to 123 labelled ok_1(2)
- 120 to 132 labelled proper_1(3)
- 120 to 133 labelled g_1(3)
- 120 to 143 labelled g_1(4)
- 120 to 140 labelled ok_1(2)
- 120 to 150 labelled proper_1(5)
- 121 to 122 labelled f_1(2)
- 121 to 127 labelled proper_1(3)
- 122 to 114 labelled mark_1(2)
- 122 to 125 labelled proper_1(3)
- 123 to 118 labelled g_1(2)
- 124 to 114 labelled g_1(3)
- 125 to 98 labelled top_1(3)
- 126 to 109 labelled ok_1(2)
- 126 to 129 labelled f_1(2), g_1(2)
- 126 to 114 labelled ok_1(2)
- 126 to 125 labelled active_1(3)
- 126 to 136 labelled f_1(2), g_1(2)
- 127 to 125 labelled f_1(3)
- 128 to 124 labelled f_1(2), g_1(2)
- 128 to 128 labelled g_1(2), f_1(2)
- 129 to 105 labelled ok_1(2)
- 129 to 114 labelled active_1(2)
- 129 to 124 labelled ok_1(2)
- 129 to 135 labelled g_1(3)
- 132 to 127 labelled g_1(3)
- 133 to 118 labelled ok_1(3)
- 133 to 135 labelled f_1(3)
- 133 to 125 labelled ok_1(3)
- 133 to 144 labelled active_1(4)
- 134 to 132 labelled ok_1(3)
- 134 to 139 labelled g_1(4)
- 134 to 151 labelled g_1(5)
- 134 to 150 labelled ok_1(3)
- 134 to 153 labelled proper_1(6)
- 135 to 114 labelled ok_1(3)
- 135 to 125 labelled active_1(3)
- 136 to 128 labelled ok_1(2)
- 136 to 138 labelled f_1(3), g_1(3)
- 137 to 114 labelled mark_1(3)
- 137 to 125 labelled proper_1(3)
- 138 to 128 labelled ok_1(3)
- 138 to 124 labelled ok_1(3)
- 138 to 138 labelled f_1(3), g_1(3)
- 138 to 142 labelled g_1(4)
- 139 to 127 labelled ok_1(4)
- 139 to 141 labelled f_1(4)
- 139 to 144 labelled ok_1(4)
- 139 to 152 labelled active_1(5)
- 140 to 125 labelled g_1(4)
- 141 to 125 labelled ok_1(4)
- 141 to 144 labelled active_1(4)
- 142 to 114 labelled ok_1(4)
- 142 to 125 labelled active_1(3)
- 143 to 125 labelled mark_1(4)
- 143 to 144 labelled proper_1(4)
- 144 to 98 labelled top_1(4)
- 150 to 144 labelled g_1(5)
- 151 to 144 labelled mark_1(5)
- 151 to 152 labelled proper_1(5)
- 152 to 98 labelled top_1(5)
- 153 to 152 labelled g_1(6)
- 154 to 153 labelled ok_1(4)
- 154 to 155 labelled g_1(5)
- 155 to 152 labelled ok_1(5)
- 155 to 157 labelled active_1(6)
- 157 to 98 labelled top_1(6)